COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require"lispub.pub[206,LSP]"source
C00005 00003	.ss Structural Induction
C00006 ENDMK
C⊗;
.require"lispub.pub[206,LSP]"source
.SECTION←4
.PAGE←74
.SEC		 PROVING LISP PROGRAMS CORRECT

	In this chapter we will introduce techniques for proving
LISP programs correct.  In general, they will be limited to
clean LISP programs.

	The  necessary basic facts can be divided into four categories:
algebraic facts about lists and S-expressions, general facts about
composition, facts about first order logic including conditional
expressions, facts about the inductive structure of lists and
S-expressions, and general facts about functions defined by
recursion.  Ideally, we would use a general theory of recursive
definition to prove theorems about LISP functions.  However,
the general theory is not well enough developed, so we have had
to introduce some methods limited to LISP functions defined by
particular kinds of recursion schemes.

.ss Algebraic facts about S-expressions and lists.

	The algebraic facts about S-expressions are expressed
by the following sentences of first order logic:

	%3∀x.(issexp x ⊃ %4at%3 x ∨ (issexp %4a%3 x ∧ issexp %4d%3 x
∧ x = (%4a%3 x . %4d%3 x)))%1

and

	%3∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬%4at%3(x.y)
∧ x = %4a%3(x.y) ∧ y = %4d%3(x.y))%1.

These axioms treat S-expressions among other objects.  If we can
assume that all objects are S-expressions or can declare certain
variables as ranging only over S-expressions, we can simplify
the axioms to

	%3∀x.[%4at%3 x ∨ x = [%4a%3 x . %4d%3 x]]%1

and

	%3∀x y.[¬%4at%3[x.y] ∧ x = %4a%3[x.y] ∧ y = %4d%3[x.y]]%1.


	The algebraic facts about lists are expressed by the following
sentences of first order logic:

	%3∀x. islist x ⊃ x = %5NIL%3 ∨ islist %4d %3x%1,

	%3∀x y. islist y ⊃ islist[x . y]%1,

	%3∀x y. islist y ⊃ %4a%3[x . y] = x ∧ %4d%3[x.y] = y%1,

.ss Structural Induction